$\forall$$A$:Type, $B$:($A$$\rightarrow$Type), $x$:$A$, $v$:$B$($x$), ${\it eq}$:EqDecider($A$), $f$:$x$:$A$ fp$\rightarrow$ $B$($x$). $f$$x$ : $v$ $\in$ $x$:$A$ fp$\rightarrow$ $B$($x$)